fetch lisp2.ax;
fetch fundef.ax;
fetch flat.stp;fetch intege.ax;fetch intege.ax;fetch intege.ax;FETCH INTEGE.AX;
EXIT;SHOW AXIOMS;
∧I induction[P←λn.(¬(n=0) ⊃ integer pred n)];
cancel;
∧I induction[P←λn.(¬(n=zero) ⊃ integer pred n)];
tauteq 1:#1#1;
cancel;
assume ¬(n=zero);
cancel;
assume ¬(n=0) ⊃ integer pred n;
cancel;
assume ¬(n=zero)⊃integer pred n;
show proof;
exit;FETCH INTEGE.AX;
ASSUME ∃n.(¬n=zero ∧ ¬integer pred(n,zero));
exit;show axioms;
assume ∃n.(¬n=zero ∧ ¬integer pred(n,zero));
assume ∃n.(¬n=zero ∧ ¬integer pred1(n,zero));
∃e 1 n;
∧i induction[P←λm.¬integer pred1(n,m)];
show axioms;
∀e pred2 n n1;
distrib λm.=(pred1(n,n1),m) 4:#2;
taut succ n1 = n ⊃ pred(n,n1) = n1 4 5;
taut succ n1 = n ⊃ pred1(n,n1) = n1 4 5;
taut ¬(succ n1 = n) ⊃ pred1(n,n1) = pred1(n,succ n1) 4 5;
show prf;
show axioms;
assume ¬integer pred1(n,n1);
∀e integer n1;
tauteq 7:#2 6 7 8 9;
cancel;
tauteq ¬integer pred1(n,succ n1) 6 7 8 9;
⊃i 8 10;
show prf;
∀i 11 n1;
taut 3:#2 2 3 12;
⊃i 2 13;
cancel;
∧i induction[P←λn.(¬n=zero ⊃ ∃m.(succ m = n))];
tauteq succ n = succ n;
∃i 15 m[occ=1];
∃i 15 m occ=1 ;
∃i 15 n←m occ=1 ;
∃i 15 n←m occ 1 ;
taut 14:#1#2#1 16;
∀i 17 n;
show prf 14;
tauteq 14:#2 14 18;
show prf 13;
show prf 1;
∀e pred2 succ m m;
distrib λn1=(pred1(succ m,m),n1) 20:#2;
distrib λn1.=(pred1(succ m,m),n1) 20:#2;
taut succ m = succ m ⊃ pred1(succ m,m)=m 20 21;
tauteq 22:#2 22;
show prf 1 13 19;
∀i 23 m;
cancel;
∀e integer m;
tauteq pred1(succ m,m) 24 23;
tauteq integer pred1(succ m,m) 24 23;
∀i 25 m;
show prf 1 13;
show prf 2;
show prf;
exit;show proof→pred.∀e 19 n;
taut 27:#2 27 2;
∃e 28 m;
substr 29 in 13;
cancel;
subst 29 in 13;
∀e 30 m;
taut false 25 30;
taut FALSE 25 30;
taut FALSE 25 31;
⊃i 1 32;
unify ∀n.(¬n=zero ⊃ integer pred1(n,zero)) 33;
taut ¬33:#1 33;
unify ∀n.(¬(n=zero) ⊃ integer pred1(n,zero));
unify ∀n.(¬(n=zero) ⊃ integer pred1(n,zero)) 33;
unify ∀n.(¬(n=zero) ⊃ integer pred1(n,zero)) 34;
unify ∀n.¬(¬(n=zero) ∧¬integer pred1(n,zero)) 34;
unify ∀n.¬34:#1#1 34;
exit;show proof 34;
push 34;
∀e 35 n;
∀e pred1 n;
tauteq ¬(n=zero)⊃ integer pred n 36 37;
∀i 38 n;
show proof→pred.prf;
close;
show commands→pred.cmd;
exit;fetch lisp2.ax[f76,jmc]
;fetch lisp2.ax;
declare opconst alt(list) [r←700];
declare OPCONST alt(list) [R←700];
axiom alt: ∀x.(alt x = if null x ∨ null cdr x then x else alt (cdr cdr x);
AXIOM ALT: ∀u.(alt u = IF NULL u ∨ NULL CDR u THEN u ELSE alt(CDR(CDR X));;
AXIOM ALT: ∀u. (alt u = IF NULL u ∨ NULL CDR u THEN u ELSE alt(CDR (CDR U)));
AXIOM ALT: ∀u. (alt u = (IF NULL u ∨ NULL CDR u THEN u ELSE alt(CDR (CDR U))));
AXIOM ALT: ∀u. (alt u = u);
;
fetch fundef.ax[f76,jmc];
fetch fundef.ax;fetch lisp2.ax,fundef.ax;
fetch lisp2.ax;
fetch fundef.ax;fetch lisp2.ax;
fetch fundef.ax;FETCH LISP2.AX;
FETCH FUNDEF.AX;FETCH LISP2.AX;
FETCH FUNDEF.AX;FETCH LISP2.AX;
FETCH FUNDEF.AX;FETCH LISP2.AX;
FETCH FUNDEF.AX;fetch lisp2.ax;
fetch fundef.ax;
∧i induction3[P←λx.LIST ALT x];
∧i INDUCTION3[P←λx.LIST ALT x];
CANCEL;
∧I INDUCTION3[P←λu.LIST ALT u]
;
cancel;
∧I INDUCTION3[P←λu.(LIST u ⊃ LIST ALT u)];
exit;